HolRefute: Quickcheck, narrowing and a Nitpick-style Kodkod model finder - #2051

ThmSetData's stored-attribute path records an ADD delta before applying
it to the global value, so a set type whose apply_to_global rejects the
theorem leaves a delta that raises again in every descendant theory.
That is an upstream bug, present independently of this work, and fixing
it belongs in its own change: restore src/1/ThmSetData.sml,
src/parse/AncestryData.{sml,sig} and the Portable.uninterruptible
primitive added for it to their upstream state.

KeyedThmSet's own export_thm keeps updating before recording -- that is
local to code introduced here and needs no shared-code change -- and the
IndDef selftest now checks only the diagnostic on the stored-attribute
path, since persistence there is governed by the upstream ordering.

path_11 exists only to supply the one_one field of the path TypeBase
entry; stopped_at_11 and pcons_11 are already exported and simp-tagged,
so the conjunction added nothing to pathTheory's public namespace.

Also drop the redundant trailing semicolons on the two Theorem
value-bindings added alongside it.

The level-2 quality gate had been un-runnable since eb9def1.  Holmake
never typechecks selftest.sml -- on Poly/ML a .uo is a load script, so
the file is compiled by quse declaration by declaration as it executes
-- and execution aborted early enough that roughly 20000 lines had never
been compiled at all, let alone run.

Kernel and harness:

  - theory_is_available asked for the current theory through
    Theory.current_theory, which raises when there is no theory segment.
    [bin/hol run] loads no prelude, so a script reaching [load "Refute"]
    hits exactly that state.  Ask the way Theory.get_parents does.
  - selftest.sml opens a scratch segment for the same reason, and
    shadows check_result so an exception from a predicate is one failed
    test rather than an aborted file: testutils.timed guards the
    function it runs but not the predicate it then applies, and the
    idiom used throughout this file does its work in the predicate.
  - the tests that enter the pipeline below refute_problem now mint the
    dynamically scoped call token themselves and release run resources
    on the way out, as refute_problem does.  Without it the smart gate
    raised "no active Refute call"; with a token but no release, a cache
    entry is stranded under a token nobody can look up again and its
    compiled_test is never closed.

Non-termination and soundness in the narrowing backend, which had never
executed because the committed module did not typecheck:

  - Refute_QC_Narrow wired retry_potential to an unbounded self-call, so
    a failed certification replay re-entered the same schedule entry for
    ever with a growing ignore list -- the list was the heap growth, and
    upd_size could not bound it because the recursion happened inside
    one entry.  Charge retries at an entry to a budget, as the random
    driver already charges its own.
  - visit_examples derived an example's genuineness from leaf values
    alone, dropping the demotion the rest of the module applies to an
    approximated domain.  Under upd_certify false this reported a
    Genuine counterexample to the true goal !x:num. ?y. y = SUC x.

Also: name the registry that actually refused when Cv rejects a type.
The custom and abstract generator registries are disjoint, so "custom or
abstract generator registered" sent the reader looking for a
register_generator call that need not exist.

Regression tests accompany each fix.  Level 1 now runs to completion in
under two minutes at ~2.4GB peak, down from a 148GB runaway; failures
are 41, all pre-existing defects this makes visible for the first time.

Eleven interactive transcripts plus a README covering the user-facing
surface: the entry points and verdicts, datatypes and functions, the
three substrates and determinism, smart generators, narrowing, custom
generators, the unused-assumption sweep, the model finder, and the
extension points.

These are session transcripts, not theory scripts -- Holmake ignores
them.  Each was run through

    bin/hol --holstate=refuteheap < examples/<file>

and the prose reconciled against what actually came back.  Files 09 and
10 need a Kodkodi component and a Java runtime; without one those calls
report Unknown rather than failing.

Several transcripts currently describe defective behaviour as though it
were designed -- the certification gap in 03, the potential-only
sections and the full-copy typedef workaround in 10, the ersatz
weakening in 11.  They need re-running and rewriting as those defects
are fixed.

register_quotient documented two accepted registration theorems and had
a destructor for each, but quotient_theorem_info only ever called
dest_bare_quotient and hardcoded the partial flag, so
dest_total_equivalence was dead code and every total extensionality
theorem was rejected as an unsupported shape.  ratTheory.RAT_EQUIV is
one, so four selftests -- the public registration validation, the frac
registration merge, the quotient axiom goldens and the refute$qn
display pins -- all died in their first registration call.

The dispatch is on the conclusion's head constant rather than on a
failed parse.  A QUOTIENT conclusion cannot also be a universally
quantified equation, so the head decides the shape outright, and each
destructor keeps its own diagnostics; parsing as QUOTIENT and falling
back to the total branch on failure would report a malformed QUOTIENT
theorem as a malformed equivalence.  The abs/rep cross-check stays on
the QUOTIENT branch alone, because a total equivalence names only the
representation relation and cannot identify supplied constants.  Both
destructors now raise one message naming both accepted shapes: neither
alone can tell which one the caller was aiming at, so the old bare
"unsupported shape" was not actionable.

The second bijection law of a typedef reached the encoding as the
exported biconditional P r <=> rep (abs r) = r.  That cannot work: for
an r outside P the value abs r is unrepresented, so the equation is
unknown rather than false, the biconditional is unknown rather than
true, and no scope of a proper-subset typedef was satisfiable.  The
model finder therefore found nothing at all for such a type, while a
whole-type typedef was unaffected -- zoo_three's own ABS/REP law had no
model at any cardinality row, zoo_univ's did.

The encoding now sees P r ==> rep (abs r) = r together with the
surjectivity P r ==> ?a. rep a = r.  The guard drops exactly the half
that mentions unrepresented values, and the surjectivity restates that
half without naming abs, so the abstract carrier stays pinned to P's
extension instead of to some subset of it; without it a typedef pinned
below its true cardinality yields spurious models.  With the membership
axiom the pair is equivalent to the biconditional, so no model is
gained or lost.  A whole-type typedef degenerates to T ==> ..., and the
registration accessor still reports the theorem's own conjuncts -- only
preprocessing sees the restatement.

The level-1 failure count goes from 41 to 37, removing exactly those
four failures and adding none.

Three defects in Refute_Extract, all in code the selftest had never
reached, accounted for nine level-1 failures.

Generated names.  556d5c6 made binder names injective, escaping every
non-alphanumeric character behind a v_ prefix, and routed upper_name and
lower_name through the same function.  Those two mint names for
generated datatype constructors and generated functions, which are
already separated by a fresh serial -- C_CONS_refute_ty_3 became
C_v_CONS_urefute_uty_u3 and f_rx_odd_1 became f_v_rx_uodd_u1 for no gain
beyond unreadable output.  Worse, the same function names SML type
variables, and the escaping ate the leading quote: :'a compiled to the
value identifier v_pa, which is not a type at all.  Injectivity now
belongs to clean_name and binders alone; sanitize_name restores mere
character legality for the names Refute mints itself.

Constructor patterns in strict mode.  fa026fc pointed strict
definition clauses at the observation matcher, so that a char-list CONS
would never be rendered as an SML pattern.  The matcher only knew how to
observe generated datatypes, but strict extraction keeps lists, options
and pairs in their native SML representations and mints no datatype for
them, so every definition matching on [] , ::, NONE, SOME or a pair
rejected the whole goal with "unknown lazy pattern constructor
list$NIL".  It now emits the native patterns the strict expression
compiler already emits for those constructors; the lazy representation,
where every type is a datatype, is unchanged.

Unrequested structural equality.  f2b0f24 stopped compile_types from
requesting equalities, but equality_declarations declared one per
registered type in strict mode regardless of what was requested, so the
removal changed nothing.  A representation-only compilation still
emitted structural equality for every type it touched, and any type
mentioning an arrow failed outright, because equality on a function has
to enumerate its domain.  Both modes now declare exactly the requested
set.  Discovery cannot widen the declared type set behind the datatype
declarations that precede it: ensure_type already registers every
constructor argument, element, domain and range type.

The byte golden moves from 3359/3964 to 3461/4157 bytes.  It was last
recorded at 6156067, before four later commits that legitimately
changed emission -- variables carry a type key since 2aebf52,
definition clauses go through the observation matcher since fa026fc,
its nonlinear patterns since 42beb32, and smart generator outputs bind
before residual checks since f66f652 -- so no fix could have restored
the old digest.  The emitted source was read in full: the strict program
is the prelude, no equality declarations, and one native list match; the
lazy program adds the hole helper, the two-constructor refute_ty_3
declaration and its suspended spine.

The level-1 failure count goes from 37 to 28, removing exactly those
nine failures and adding none.

Eleven level-1 failures across the model-finder translation pipeline
came from one library defect and five stale goldens.

The defect is a8e7d31.  It wanted a partially applied BIT1 to
translate, and got there by dropping NUMERAL, BIT1 and BIT2 from
built_in_consts.  But that table is what every earlier stage consults:
def_props_for_const, unfold_defs_in_term, specialize_consts_in_term,
add_to_uncurry_table and box_type all ask is_built_in_const, so a
literal 5 stopped being a numeral to all of them.  It was unfolded and
specialized into refute$sp3$arithmetic$NUMERAL with the definitional
axioms BIT2 = ZERO + (ZERO + SUC (SUC 0)) in tow -- unary arithmetic,
which is exactly what the comment a8e7d31 deleted had warned about.
Binarization then never triggered, skolemization and case unfolding
goldens drifted, and the live bridge stopped firing smart binary
integers.  The skeleton goes back on the table and the nut layer, which
already recognizes a fully formed numeral before it looks at heads,
expands what is left: NUMERAL n as n and BIT1/BIT2 n as 2n + 1 and
2n + 2.  A bare constructor eta-expands into the same case rather than
reaching the arity-0 built-in branch, whose only outcome for it was to
raise.  That fixes the built-in count and never-unfold pins, all five
preprocessing goldens, and one live-Kodkodi failure.

Five goldens recorded behaviour their own commits had already changed.

min_univ_card_of_rep of Opt (Struct [Atom (2, 0), Atom (3, 2)]) was
pinned at 6.  An Atom (k, j0) occupies indices j0 .. j0 + k - 1, so
Atom (3, 2) reaches index 4 and demands 5; the implementation has said
k + j0 since 670b9b1, which introduced both halves, so the golden was
arithmetic that never held.

The scope facto pins predate 79c8070, which made concreteness quantify
over the constructor argument types rather than over the binder types of
each argument type -- the latter is empty for every first-order field, so
the old test only ever exercised the trivial case.  A num list whose num
is capped at an inexact 2 is now inconcrete under both facto values, and
therefore exact under neither; completeness still carries the
facto-sensitivity the test was written for.

certify's Discarded arm returned a Potential carrying "certification
refuted the model" until 8d7f8c1 made it Drop, on the ground that
kernel evaluation has refuted the assignment at every certainty level.
Its Certified arm stopped merging decoded solver values into the
evaluations at 569bbc4 and stopped attaching the reconstruction report
at 96676da.  The certified eval is now the kernel's own, which for the
underspecified HD [] is the term itself, and the test pins model = NONE
as well.

certification_copy has taken the reconstruction's per-type atom rows
since c16c124, so that custom atom names certify; the merged-type-var
fixture still passed types = [] and could no longer produce an atom
substitution.  It now carries the row MFM.reconstruct produces.

tests/mf-binary-integers.kki still encoded Num as Isabelle's clamping
nat, if i <= 0 then 0 else i.  HOL4's Num is @n. if 0 <= i then i = &n
else i = -&n, that is ABS (integerScript.sml:1888, with Num (-a) = Num a
at 1946), and fd828ee corrected the translation without regenerating
the golden.  tests/forl-expressions.kki was hand-edited by c2c8766
rather than regenerated: that commit made the bitwise operators
parenthesize their right operand, which changes 1 & (2 & 3) and
1 | (2 & 3) but not the left-nested BitXor (BitXor (1, 2), 3), whose
correct rendering stays 1 ^ 2 ^ 3.

The level-1 failure count goes from 28 to 16, removing exactly these
eleven plus "smart binary integers did not fire on the arithmetic goal"
and adding none.

Two of the nine live-Kodkodi-bridge failures were library defects, and
they are independent of each other.

79c8070 rewrote the concreteness test of a data type spec to demand an
exact cardinality of every constructor field, on the reading that an
inexact field makes the encoding inexact.  But that is what completeness
already says.  Concreteness asks the narrower question of whether one
atom of the encoding can stand for two different values, and only a
function-typed field can do that, and only when its domain is inexactly
represented -- which is why the test quantifies over the binder types of
the field types rather than over the field types themselves, and why a
first-order field contributes no condition at all.  Conflating the two
made every recursive data type over an infinite type inconcrete, and
choose_reps_in_nut translates a positive equality on an inconcrete type
to False in the sound problem.  With :num capped at 2, ``xs = [0]``
therefore assembled to False and came back UNSAT, so the scope-to-Kodkodi
harness saw its satisfiable list problem refuted and every counterexample
that pins a list to a literal was silently unreachable.  The facto pins
in mf_scope_offsets_and_facto_pairs go back to (true, true) for a num
list, which is the value 0b1d430 recorded and 3b330f2 rebaselined to
match the defect.

2aeab37 made a semantically weakened model search inconclusive, to stop
an UNSAT run over a whacked or ersatz-substituted formula from being read
as NoCounterexample.  That is right, but the guard it added preempts the
Counterexample arm as well, so a model the search did find was discarded
too.  Weakening is a property of the formula the solver saw; it is
already recorded in the reasons of each reconstructed counterexample, and
a counterexample the kernel went on to certify does not depend on how the
search reached it.  The guard now applies only when there is nothing to
report.  This is also what the level-2 inv/O acceptance cases need: the
rational Frac encoding is an ersatz registration, so any goal that
touches it sets the flag.

The remaining seven failures in the group are one question, not seven.
Each reports "untrusted Kodkodi model; no HOL certificate", which is the
base certainty 3948a7b installed when it required a HOL certificate for
a genuine Kodkodi model.  Their goals -- Hol_reln and Hol_coreln
predicates, RTC, inv and O -- are gated non-executable, so certify never
calls Refute_Cert at all, and computeLib gets stuck on them even when
asked directly.  Five of the seven additionally pin cert = NONE, so they
can only ever be satisfied by the fallback_certainty path that 3948a7b
left dead.  They are left failing: the tests date from 20 and 21 July and
record the policy that the 29 July certification commits replaced, and
resolving that is a policy decision rather than a defect.

The level-1 failure count goes from 16 to 14, adding none.

Seven level-1 failures were left after the model-finder work: one
library defect, one stale golden, and five invalid test fixtures.  They
have four independent causes.

The defect is 8cd6a04.  It replaced the diagonal instantiation of
type variables with their Cartesian product, on the ground that the
diagonal never tries rf2 against rf3.  But an instance's card is not a
free index: preprocess_forms builds instance k by interpreting every
type variable as rfk, and the rest of the pipeline reads card back as
that cardinality.  Refute_QC.schedule orders its work by card + size,
which is only a cost if card is the size of the type; the plan dump,
the counterexample message and the model-finder stats all print it as
the cardinality tested.  Numbering the product consecutively left card
a bare dispatch index, so the schedule stopped ordering by cost and the
reports named a number with no meaning.  It also made preprocessing
build finite_type_size raised to the number of type variables
instances, each carrying its own normalization and executability scan,
before any backend runs -- 81 of them for a four-variable goal at the
default size of three.  That restores the three preprocessing and
dispatch tests, which have pinned rf1 through rf3 since 15 and 19 July
and which 8cd6a04 did not update.

The stale golden is the depth bound in pnf_engine_units.  It was
written on 22 July against length position < depth and still expects
depth one to refuse every refinement.  09be56b corrected that bound
to length position <= depth + 1, which is exactly what the scheduled
depth's shape describes: shape_of d reaches term depth d, that is tree
positions of length d + 1, as the neighbouring completeness pins for
shape_of 0 bool and shape_of 1 (bool option) record.  Under the old
bound the shape was always two levels deeper than the search could
reach, and depths zero and one were the same probe.  The case now cuts
off where the bound really bites, at depth zero on the nested branch
shape, and still asserts that an unreachable refinement becomes
Unknown.

The two backend-racing fixtures assume a parallel race.
Multithreading.max_threads is one in any session not given --mt, which
is how bin/hol run selftest starts, and ParList.get_some then degrades
to a sequential walk.  The genuine stub waits for the potential stub to
start, so sequentially it could only burn the two-second backend
timeout and contribute nothing, leaving the potential result to stand.
Both now raise the worker count for the duration of the race, as the
narrowing-shape and frac-registry races in this file already do.

The custom-generator fixture registers finite_custom for :ind while
returning the numeral 0.  eb4573c added the type check that catches
exactly this and adjusted the direct random_value call to name :ind
without noticing that the values were of type :num.  :ind has no
numeral syntax; num$ZERO_REP is its one built-in inhabitant, and the
fixture now produces it.

The level-1 failure count goes from 14 to 7, adding none.  The seven
that remain are the Kodkodi certification policy question 1b9aaba
described, untouched.

The seven remaining level-1 failures are the certification policy
question, and the answer is that the documented trust model wins.  The
tests are wrong, not the library.

They were written on 20 and 21 July (645f5c0, a974d21, 4115585),
when a model-finder reconstruction could still be promoted on
translation-side confidence alone.  3948a7b then settled the trust
model: Kodkodi is an accelerator, not a proof oracle, so a
reconstructed assignment stays Potential until Refute_Cert establishes
the HOL counterexample.  520eea4 wrote that into README and
Manual/Description/Refute.smd, where it now reads "a model-finder
result is Genuine only with" a certificate.  The seven tests were never
re-run against the policy that superseded them, because the selftest
only became runnable again afterwards.

No certificate can exist for these goals.  All seven refute a
proposition over a non-executable constant -- refuteTableZoo's
inductive and coinductive fixpoints, RTC, inv, and O -- so Refute_Cert
re-evaluates the instantiated proposition and gets stuck: for the RTC
smoke computeLib returns the identity
|- ~(\x y. x = 0 /\ y = 1)^* 0 1 <=> ~(\x y. x = 0 /\ y = 1)^* 0 1.
Kodkod does find a model, and the model is right; what is missing is a
kernel witness for it.  Expecting Genuine here asks the invariant that
Genuine implies a certificate to be broken.

So each of the seven now pins Potential ["untrusted Kodkodi model; no
HOL certificate"] where it pinned Genuine.  Nothing else about them is
relaxed.  Every test still requires a kodkod counterexample with a
reconstructed model report, and the iterator-scope pins, the
no-iterator pin for the starred linear predicate, and the goals
themselves are unchanged.  The two that pinned no certificate field at
all now pin cert = NONE, and all seven gained model = SOME _, so the
Genuine-implies-certificate invariant is asserted from both sides
rather than assumed.

Refute_ModelFinder_Model's fallback_certainty went dead when 3948a7b
made Potential unconditional, and it is the one function in the file
that could return Genuine without a certificate.  Left in place it is a
soundness trap for whoever next needs a certainty in that neighbourhood,
so it is deleted.  Its genuine_means_genuine argument survives as a
field of certify's record, unread since the same commit; the field
stays for source compatibility but is now matched by a wildcard under a
comment saying why nothing may act on it.  certify's sound flag is not
vestigial -- it still gates the warning on a refuted model -- and the
executable gate in Refute_ModelFinder is untouched, since it also
drives kodkod_certainty_ceiling.

The level-1 failure count goes from 7 to 0.  The outcome count is 701
either way: the seven flipped, and the failure set gained nothing.

The level-2 quality gate did not finish.  Two bounded runs, one of an
hour and one of four hours, died at the same log line inside "Refute
Enum snapshot restoration" having produced identical output: no CPU,
no memory growth, and nothing further ever printed.

The wedge is a self-deadlock on theory_mutex, and the concurrent
section of that test has nothing to do with it.  Refute_EvalCv forces
generator synthesis, definitions and cv translation while compiling,
so that a translation failure surfaces as inapplicability while Auto
can still choose another substrate; that work runs inside the held
theory bracket, which then stays open until the compiled test is
closed.  The test compiles a compute test and a cv test from one goal
and only afterwards runs them, so the compute test's first run opened
a second bracket on the thread that already held the first, and
lock_interruptibly spun on a trylock that could never succeed --
silently, because the spin sleeps 10ms between attempts.  Reversing
the two executions makes the test pass, concurrent section included;
that is what identified the lock rather than the futures.

Overlapping compiled-test lifetimes are legitimate, so the bracket is
now re-entrant for the thread holding it.  A nested open shares the
outer baseline and only the outermost close reverts and unlocks, which
leaves the hygiene invariant where it was: the theory is clean again
exactly when no bracket is open, and one revert retires every artifact
made under any of the nested brackets.  Other threads still wait,
because HOL's theory state still tolerates a single mutator.

The regression test is level 1 and bounded.  It holds a bracket open,
nests a with_clean_theory inside it, and runs that under Timeout.apply
so a future regression is one failed test instead of a four-hour wedge
of the gate.  On the old code the nested call times out; on the new
one it returns and the snapshot is restored.

"Refute corpus: ParList get_some lets a loser unwind" asserts that a
losing worker is interrupted rather than killed, so that it cannot
leave the theory mutex locked behind an uninterruptible section.  It
never observed that: ParList.get_some forks nothing at or below one
thread and falls back to get_first, and `bin/hol run selftest` starts
with Multithreading.max_threads at one.  The sequential walk answered
from the winner, the loser never ran, and the flag the test reads
stayed false.  A probe confirms it: at one thread the trial reports
unwound=false, at two it reports unwound=true.

The check now runs under with_raced_backends, the bracket the other
concurrency tests in this file already use to raise the thread count
and put it back.  What it asserts is unchanged; it simply gets the
second worker its assertion needs.

Refute trusts Kodkodi exactly as Isabelle/HOL's Nitpick trusts Kodkod,
and must never be stricter.  Write that down where it cannot be lost:
this rule has now been broken once and re-derived at some cost.

`certainty` and `cert` are independent axes.  `certainty` is the
semantic strength of the result -- whether the encoding was sound and
exact, which is Nitpick's genuine / quasi-genuine / potentially spurious
distinction -- while `cert` records only whether Refute happened to
build a HOL theorem.  A model-finder result may be `Genuine` with
`cert = NONE`, exactly as a QC hit is under `certify=false`.  The
README asserted both this and its opposite two sentences apart; the
opposite is now gone.

Collapsing the axes does more than mislabel results.  Once no model can
be promoted, the `max_potential` budget starves and found models are
discarded, so the model finder answers `Unknown` on goals where it has
computed a concrete counterexample -- 94 such cases at level 2.

3948a7b introduced the rule in seven lines on 2026-07-29 and
2db1913 re-baselined seven tests to match it.  Both are being
reverted.  Tests expecting `Genuine` with `cert = NONE` from kodkod
encode the intended semantics and are correct as written.

Refute_SmartGen registers a theory hook that retires the whole
enumerator cache on any TheoryDelta.  The evaluator's snapshot/revert
bracket is full of such deltas: the definitions and cv translations it
makes, and the deletions its revert performs.  None of them say anything
about the relations the enumerators were inferred from -- every constant
the bracket adds is private and freshly named, and the revert restores
the baseline exactly.

Retiring the cache on them broke a promise the plan had already made.
Planning records an Enum node naming a program; a substrate then defines
something; the next substrate compiled from the same plan no longer
finds the program and reports

    smart plan: missing top-level enumerator program

which surfaced at two level-2 selftest sites and in
theory_tests/refuteCvCleanScript, where it also stopped
refuteCvCleanCheckTheory from ever running.

So the hook now ignores deltas between enter_private_theory and the
matching leave_private_theory, a depth counter under the existing cache
mutex.  Refute_EvalEnum enters right after acquiring theory_mutex and
leaves after close_theory_bracket, so the revert's own deletions are
covered too.  The suppression is safe because the bracket holds HOL's
single-mutator lock across exactly that span, so no user theory change
can hide inside it, and programs whose relation genuinely did go stale
are still dropped by the existing Theory.uptodate_term freshness check.

Level 1 stays at 0; with the library fix stashed the new test is the
only failure.  Level 2 loses both "missing top-level enumerator program"
sites (the string now occurs zero times).  The four other level-2
movements are kodkod JVM timeouts under load -- three tests that each
failed on one solver and passed on the other now fail on both, and the
"kodkod timed out" count goes 10 to 13.

The owner has ruled the certificate-required policy wrong.  HolRefute
trusts Kodkodi exactly as Isabelle/HOL's Nitpick trusts Kodkod and must
never be stricter.  This undoes 3948a7b ("require HOL certificates for
genuine Kodkodi models") and 2db1913 ("re-baseline seven Kodkodi
smokes to the trust model"), together with the four commits that had
adapted the rest of the suite to them -- 7325c52, cfdf166,
5af24a8, 62e82d5 -- and the relaxation 573643e.

`certainty` and `cert` are two independent axes.  `certainty` is the
semantic strength of the result and comes from the encoding's soundness
and exactness, mirroring Nitpick's genuine / quasi-genuine / potentially
spurious.  `cert` records only whether Refute also built a HOL theorem.
There is no invariant that Genuine implies a certificate: a model-finder
result is legitimately Genuine with cert = NONE, exactly as a QC hit is
under certify = false.

Refute_ModelFinder_Model.fallback_certainty comes back and decides the
verdict from `sound` and `genuine_means_genuine` again.
kodkod_certainty_ceiling again reports the certainty the encoding can
reach: a ceiling that underestimates hides a stronger result and
violates the backend contract.  The seven Kodkodi smokes, the model
certification and polymorphic-model protocol unit tests, the ceiling
unit test, the quotient/typedef acceptance test and about ninety
acceptance-corpus expectations pin the encoding-derived verdict again.
Manual/Description/Refute.smd now states the two axes; README and
CLAUDE.md already record the decision as settled.

"Manual_Nits HD append" moves the other way, from ExpectPotential to
ExpectGenuine: the search reaches a genuine model on that goal, which
the certificate rule had been capping.

Level 1: 0 failures over 703 outcomes.  Level 2: 50 failures, down from
156 at ef95af3, with 107 distinct failing test names resolved and no
certification-family failure left.  theory_tests: 6/6, including
refuteRegistrationClean, which this policy was breaking.  What remains
at level 2 is pre-existing: the max_potential = 0 "every model found was
discarded" group, the rat ersatz group, the narrowing needle golden, the
GSPEC conformance case, the cv/compute corpus timeout, and
load-sensitive timeouts.

The transcripts under src/HolRefute/examples/ still narrate the reverted
policy and need re-running by hand.

92c24de is the eighth member of the family 19aa93b reverted, and it
was missed because its diff changed budget arithmetic rather than
swapping Genuine for Potential.  Its own comment stated the reverted
rule verbatim: "Reconstruction can only establish genuineness by
producing a certificate.  Charge the model to the certainty it actually
has, rather than to the sound solver problem that yielded it."

Acting on that, harvest charged max_potential for every model whose
certainty was not Genuine -- including QuasiGenuine -- and at
max_potential = 0 discarded it and set discarded_sound_model, so the
search answered Unknown "every model found was discarded".  The tell was
internal disagreement: keep_counterexample counts met_potential by
certainty_is_potential, harvest charged by not certainty_is_genuine, so
a QuasiGenuine model was charged against a budget it was never counted
in.  Measured on zoo_wf_lfp n ==> n = 0 under kodkod/MiniSat_JNI, one
scope and one model gave three verdicts: (wf=true, max_potential=0)
Unknown; (wf=true, max_potential=1) QuasiGenuine; (wf=smart,
max_potential=0) Genuine with cert = NONE.

max_potential bounds models that may be spurious because their encoding
is unsound, so only the liberal problems spend it.  A sound problem's
model is a real result whatever certainty reconstruction lands on, so
the sound branch harvests take_at_most max_genuine again and keeps every
model that reconstructs, and only a genuine model spends a max_genuine
slot, as upstream counts num_genuine.

Kept from 92c24de: the keep_counterexample extraction, so a
counterexample is registered only when it is actually kept rather than
as a side effect of reconstruct, and the harvest loop in place of the
old List.mapPartial.

The exhausted-search test at :1122 needed null cexs added.  It read an
untouched budget as "the search delivered nothing", which a sound
problem can now satisfy while holding a model, and would have reported a
real result as an exhausted search.

Level 1: 0 failures.  Level 2: 50 to 35, no new failures; the 14
predicted resolve (Core_Nits boxed relation, relation dont_box, function
argument dont_box, and Refute_Nits weak drinker, predicate of Eps, Eps
equality, T3 constructor, on both solvers), plus the known
scope-fusion flake.  theory_tests 6/6 OK.

Ersatz.  An ersatz entry names a surrogate that denotes the same
function as the constant it replaces, chosen only because the model
finder can encode it: CARD as card', and each rat operation as its
normalized Frac counterpart, whose faithfulness argument is spelled out
in refuteScript (every frac-valued operation normalizes, so canonical
pairs are in bijection with the rationals).  Registering an entry
asserts that equivalence, exactly as upstream Nitpick's ersatz_table
does, and upstream records nothing when one fires.  A faithful
substitution changes no model in either direction, so it may not raise
a weakening flag.  It did, and because the Frac encoding for rat is
registered by default, that made every scope-exhausting rat search
report Unknown instead of NoCounterexample: 26 of the 35 residual
level-2 failures.

Whack.  Not inverted, and not the same kind of thing, so the flag is
now whack-only.  refute$unknown is not an unconstrained relation the
solver may pick: the nut translation maps it to Cst Unknown, which
becomes the empty relation in term position and, in formula position,
False at positive polarity and True at negative, and
choose_reps_in_nut flips that polarity for the liberal sibling of every
problem.  Whacking is therefore encoded exactly like an unrepresentable
value, and its approximation direction always follows the problem's own
soundness flag: a sound problem's SAT stays conclusive, and a liberal
problem's UNSAT, which is what NoCounterexample rests on, stays
conclusive too.  Unrep arises in every undersized scope and raises no
flag; whack cannot need one either.  The guard that turns a whacked
absence into Unknown is thus conservative rather than forced.  It is
kept, because whack is opt-in and explicitly requested, but its comment
asserted the invalidation was forced and is corrected in place.  A
found model still carries its weakening reason.  No verdict becomes
stricter anywhere.

The regression test pins the defect: a true rat law under the default
Frac/ersatz registration, with every scope exhausted, must be
NoCounterexample rather than Unknown.  It sits at level 1, one goal and
a few seconds, beside the other targeted model-finder regressions.

Measured here: level 1 = 0 failures.  Level 2 = 8 failures against the
35-failure baseline at a25f23e, removing all 26 rat rows plus the
known flake "Refute Enum substrate conformance" and adding none; the
remaining 8 are all in the baseline set (narrowing backend, full
substrate conformance matrix, 4 x Typedef_Nits 05/06 one_or_two,
Manual_Nits subst2).  theory_tests 6/6.  Examples 09, 10 and 11 were
re-run and their transcripts corrected: the deliberately wrong MAX/MIN
ersatz swap in 11 now returns the wrong answer it always implied,
instead of hiding behind an Unknown.

Mechanism.  Refute_QC.bounded_close ran every substrate cleanup under
Timeout.apply with a 100ms bound.  Timeout.apply cancels by interrupting
the calling thread, and cleanup here is work that may not be torn in
half: Cv reverts its per-call theory snapshot inside
Thread_Attributes.uninterruptible, because a half-reverted snapshot
would strand Refute definitions in the user's theory, which is exactly
the invariant the cleanup exists to keep.  Poly/ML defers a masked
thread's interrupt until the mask ends, so the timer could never preempt
that revert; the interrupt landed only once the revert had already done
all of its work, and Timeout.apply, seeing its request fired and an
interrupt pending, reported TIMEOUT for a cleanup that had in fact
succeeded.  strategy_run releases the close result on the success path,
so that spurious Timeout.TIMEOUT escaped the backend, and run_backend,
which cannot tell an inner TIMEOUT from its own expired deadline, turned
it into Unknown ["exhaustive timed out"], discarding a counterexample
the search had already found and certified.

Evidence.  Instrumenting bounded_close and run_backend on the first goal
of theory_tests/refuteCvCleanScript ((tree : clean_tree) = CleanLeaf 0,
Cv substrate, backends restricted to ["exhaustive"], 10s budget):

  [DBG bounded_close TIMEOUT after 0.128s]
  [DBG run_backend exhaustive TIMEOUT after 2.997s budget 10.000s]

The cv counterexample was found and certified inside three seconds of a
ten-second budget and was then thrown away by a cleanup that had run to
completion in 128ms.  Raising the goal's budget to 120.0 does not help,
because the budget was never what expired: interactively, on one heap, a
10.0 call on this goal succeeds and a following 120.0 call fails.

Attribution.  This is not a regression from 3d2682f, and the A/B that
appeared to show one was confounded by machine load.  The first cv close
of that script, measured with identical instrumentation on alternating
builds, costs 0.052-0.111s on a25f23e's model-finder sources and
0.060-0.255s on 3d2682f's, against the same hard 0.100s bound; five
clean runs of each arm under equal conditions failed once each (pre
0.111s, HEAD 0.254s), while under load HEAD failed five out of five.
The defect is a pre-existing knife edge, since a correct cleanup
routinely costs more than 100ms, and not a behaviour change in the model
finder, which this goal never reaches: backends are ["exhaustive"] and
the sole reported reason was "exhaustive: exhaustive timed out".  The
same defect accounts for the unnamed eighth failure in the level-2
baseline, "raised: TIMEOUT 0.155 / cv disagreed with compute on the
corpus slice".

Fix.  bounded_close records completion inside a mask it owns, so a
cleanup that reached its end is a success however long it took and only
one that never got there is reported.  The Timeout.apply wrapper stays
for the independent interrupt budget that keeps an already-expired run
deadline from aborting the cleanup; it now classifies the cleanup rather
than pretending to preempt work that masks interrupts.  The regression
test registers a compute substrate whose close performs the real cleanup
and then spins 400ms masked, and requires the verdict to survive; on the
old bounded_close it fails with "raised: TIMEOUT 0.400".

Measured here: Holmake clean.  theory_tests 6/6 OK on three consecutive
clean runs, including refuteCvCleanCheckTheory, against 1-of-5 and
5-of-5 refuteCvCleanTheory failures before.  Level 1 = 0 failures.
Level 2 = 7 failures against the 8-failure baseline at 3d2682f,
removing the cv corpus-slice TIMEOUT and adding none; the remaining 7
are all in the baseline set (narrowing backend, full substrate
conformance matrix, 4 x Typedef_Nits 05/06 one_or_two, Manual_Nits
subst2).

Backends declare a family (Quickcheck, ModelFinder or Other), and
QuickcheckBackends takes the registered Quickcheck family instead of
Refute_QC's hard-coded name list, which also named the narrowing
backend Refute_QC does not own.

Refute_Core.sig and the Refute facade each listed the config types and
all ~70 updaters; both now include Refute_Config, the facade realising
its datatypes as Refute_Core's so the two stay one type.

Extract spelled the literal test out three times.  The enumerator's
clause-pattern copy lacked word literals, so a word-literal clause
input compiled to an unguarded wildcard.  No outcome is known to
change: a downstream check already filtered the extra candidates.

The three candidate counters travelled as string-keyed stats and were
re-parsed, summed and re-rendered in QC, EvalCompute and EvalSML.
Refute_Core now owns the qc_counters record, its one rendering into
stats and its one summary text, shared by QC's vacuity reason and the
witness line.

The four num/int orders were listed in MF_HOL, twice in Nut and in
Mono; MF_HOL's order_consts now feeds all of them.  Nut's arithmetic
if-chain is a key table, and Nut checks at load that its word and
char operator tables name exactly MF_HOL's built-in constants.

A backend record now carries an optional render hook returning the
scope, bindings and model text of a counterexample; kodkod supplies
it, and the scope/model/boxed-type display code moves from Refute_Core
into Refute_ModelFinder.  Backends without a hook show their bindings
with format_term.

format_term prints Quot terms through a user printer on a copy of the
grammar instead of a placeholder substitution, so long terms containing
Quot now wrap at their real width.

The model finder's codatatype, quotient, typedef and frac registries
become one operator-keyed table of classifications, so a type
operator can have only one.  A registration replaces only its own
kind; the one exception is Frac, which replaces a quotient or typedef.
Built-in codatatypes and fmap's synthetic encoding count as
classifications too, so a typedef registration over fmap is now
refused.

harvest_typedef now answers only for genuine typedefs, which removes
the need for Refute_QC.transportable_typedef's raw_typedef_data guard
against the synthetic frac/fmap entries.

Refute_Core.call_memo memoises a builder for the running call,
backends included: concurrent callers wait for the first build.  The
model finder's definition/nondefinition tables and the certainty
ceiling's nondefinition scan use it, so QC's smart context, every
model-finder instance and harvest restarts share one build.

Measured on find_unused_assms over sumTheory (2s probes): 16 table
builds at ~15ms in 22-23s, about 1%, so no cross-call cache.

Fourteen structures kept their signature inline, three of them as an
anonymous `:> sig ... end`.  Each now has X.sig declaring signature X,
ascribed `structure X :> X`, and the two uppercase signature names
(REFUTE_PROP_SAT, REFUTE_MODEL_FINDER_MONO) follow the structure name.
Interfaces are unchanged.

Refute_Config, which holds only a signature, stays a .sml: holdep makes
every reference depend on Refute_Config.uo, which a lone .sig cannot
provide.

TypeBase's accessors read the live context, so a Refute call given an
older context saw datatypes defined after it, and a tactic's reads were
reported as ambient reads inside a proof.

Refute_TypeBase mirrors the twelve TypeBase functions Refute uses over
Refute_Session.context, the running call's view, and every call site
goes through it.  Outside a call the view is the live context, so
top-level entry points are unchanged.  Refute writes no TypeBase entry
during a call, so a frozen view misses nothing the call made itself.

load compiles a module's sources in the caller's top level, so after
`open realTheory` the pervasive abs is the theorem of that name and
load "Refute" failed with type errors.  process_docfiles runs every
docfile in one session, and Conv.MP_CONV opens realTheory before the
Refute docfiles load the library.

Feedback.emit_MESG, emit_WARNING and emit_ERR switched their flag off
and left it off, so every later docfile in the shared process_docfiles
session rendered without HOL messages, warnings or error details,
among them the Refute tactics' counterexample reports.

With warnings no longer suppressed across docfiles, the
Parse.set_known_constants example prints the PROD_IMAGE overload name
in its output, and reference.pdf failed with "Unicode character Π
(U+03A0) not set up for use with LaTeX".

Export validated codatatype, typedef and quotient descriptors through theory data, with lazy replay and atomic selected batches. Preserve session registration precedence, retained proof inputs and context cache semantics.

Cover fresh-process loading orders, ancestry replacements, anonymous proofs, batch failures and theory hygiene. Document the new export APIs.

Serve replay-cache hits without a harvest transaction, comparing histories
by pointer before encoding.  Keep one kind-compatibility table, one
registry writer and shared message helpers; restore plain handlers where
no registration lookup is reachable.

Tidy the tests: named records, testutils helpers, a pattern rule for the
persistence drivers, plain load literals and no unused fixtures.